the_w:World, l:IdLnk, t:. rcvs(l;t)  (Action(destination(l)) List) 

latex

Definitions	x:A. B(x), , t  T, rcvs(l;t), {i..j}, i  j < k, P & Q,
Lemmas	filter wf, w-action wf, ldst wf, w-isrcvl wf, map wf, int seg wf, w-a wf, le wf, upto wf, nat wf, IdLnk wf, world wf